Challenge 23: Verify safety of Vec functions part 1#569
Challenge 23: Verify safety of Vec functions part 1#569Samuelsills wants to merge 3 commits intomodel-checking:mainfrom
Conversation
Add Kani proof harnesses for all 36 Vec functions specified in Challenge model-checking#23, including from_raw_parts, set_len, push, pop, insert, remove, swap_remove, truncate, drain, split_off, append, retain_mut, dedup_by, extend_from_within, extract_if, and other core Vec operations. Resolves model-checking#284 Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Verification Coverage ReportFunctions Verified (36/36 ✅)
UBs Checked (automatic via Kani/CBMC)
Verification Approach
|
There was a problem hiding this comment.
Pull request overview
Adds a Kani verification module (#[cfg(kani)] mod verify) in alloc::vec with proof harnesses covering a large set of Vec APIs as part of Challenge #23 (pointer arithmetic / safety validation).
Changes:
- Reworked the existing
verify_swap_removeharness to a simpler bounds-checked index + postcondition. - Added many new Kani proof harnesses for additional
Vecmethods (mutation, raw parts conversions, iteration, spare capacity APIs, etc.). - Introduced a
Vec::leakharness that attempts to reclaim leaked memory for verification runs.
| unsafe { | ||
| drop(crate::boxed::Box::from_raw(leaked as *mut [i32])); | ||
| } |
There was a problem hiding this comment.
verify_leak attempts to “unleak” the returned slice by converting &mut [i32] into Box<[i32]> via Box::from_raw. This deallocation is only sound if the Vec’s allocation has no excess capacity (i.e., capacity == len) and uses the global allocator; otherwise the dealloc layout can mismatch the original allocation, which is UB. Prefer not deallocating here (accept the leak in the harness), or restructure the harness to avoid Vec::leak cleanup via Box::from_raw (e.g., only perform such cleanup when you can guarantee capacity == len).
| unsafe { | |
| drop(crate::boxed::Box::from_raw(leaked as *mut [i32])); | |
| } |
| #[kani::proof] | ||
| pub fn verify_push() { | ||
| let arr: [i32; ARRAY_LEN] = kani::Arbitrary::any_array(); | ||
| let mut v = Vec::from(&arr); | ||
| v.push(kani::any()); | ||
| assert!(v.len() == ARRAY_LEN + 1); | ||
| } |
There was a problem hiding this comment.
Several harnesses in this #[cfg(kani)] module call Vec APIs that are themselves #[cfg(not(no_global_oom_handling))] (e.g., push, reserve, insert, into_boxed_slice, extend_from_within, append). Under a build that enables no_global_oom_handling together with kani, these harnesses won’t compile because those methods are not available. Consider adding matching #[cfg(not(no_global_oom_handling))] gates to the affected proof functions (or otherwise gating the whole verify module) so cfg combinations remain buildable.
Summary
Add Kani proof harnesses for all 36 Vec functions specified in Challenge #23:
from_raw_parts,from_nonnull,from_nonnull_in,into_raw_parts_with_alloc,into_boxed_slice,truncate,set_len,swap_remove,insert,remove,retain_mut,dedup_by,push,push_within_capacity,pop,append,append_elements,drain,clear,split_off,leak,spare_capacity_mut,split_at_spare_mut,split_at_spare_mut_with_len,extend_from_within,into_flattened,extend_with,spec_extend_from_within,deref,deref_mut,into_iter,extend_desugared,extend_trusted,extract_if,drop,try_fromAll harnesses verified locally with Kani.
Resolves #284